ecl{-}trans{-}halt2(${\it ds}$; ${\it da}$; $A$)($n$,$L$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$\uparrow$(ecl{-}trans{-}h($A$)($n$,ecl{-}trans{-}state($A$; $L$)))